using System;
using System.Collections.Generic;
using System.Text;
using Algorithms;
using Base;
using System.Collections.ObjectModel;

namespace PetriDiagram.Algorithms
{
    public class StateSpaceAnalysis
    {
        private bool bounded;
        private bool deadlock;
        private bool safe;
        // shortest path to deadlock!
        private List<int> pathToDeadlock;

        public StateSpaceAnalysis()
        {
            pathToDeadlock = new List<int>();
            Reset();
        }

        public void Reset()
        {
            bounded = false;
            deadlock = false;
            safe = false;
            pathToDeadlock.Clear();
        }

        public bool Bounded
        {
            get { return bounded; }
            set { this.bounded = value; }
        }

        public bool Safe
        {
            get { return safe; }
            set { this.safe = value; }
        }

        public bool Deadlock
        {
            get { return deadlock; }
            set { this.deadlock = value; }
        }

        public ReadOnlyCollection<int> PathToDeadlock
        {
            get
            {
                return pathToDeadlock.AsReadOnly();
            }
        }

        public void CountPathToDeadlock(Vertex v)
        {
            this.pathToDeadlock.Clear();
            List<int> path = new List<int>();
            Vertex actual = v;
            while (!actual.IsRoot())
            {
                path.Insert(0, actual.ComingTransition);
                actual = actual.Parent;
            }

            if ((this.pathToDeadlock.Count == 0) ||
            ((this.pathToDeadlock.Count > 0) && (this.pathToDeadlock.Count > path.Count)))
                this.pathToDeadlock = path;
        }

        public void CheckBoundless(List<MarkingVector> oldMarkings,
            List<MarkingVector> markings)
        {
            this.CheckBoundless(oldMarkings);
            this.CheckSafety(markings);
        }

        private void CheckSafety(List<MarkingVector> markings)
        {
            this.safe = true;

            foreach (MarkingVector v in markings)
            {
                for (int i = 0; i < v.Length; i++)
                {
                    if ((v[i] == MarkingVector.omega) || (v[i] > 1))
                    {
                        this.safe = false;
                        return;
                    }
                }
            }
        }

        private void CheckBoundless(List<MarkingVector> markings)
        {
            this.bounded = true;

            foreach (MarkingVector v in markings)
            {
                for (int i = 0; i < v.Length; i++)
                {
                    if (v[i] == MarkingVector.omega)
                    {
                        this.bounded = false;  
                        return;
                    }
                }
            }
        }
    }
}
